semanticsOf XSPEM

rule tick
for P timeVal
rewrite
    {
    object P : process =
        {
            time : int = (timeVal => [timeVal + 1]);
        }   
    }   
then
 {
  print("tick");
  print(timeVal+1);
 }  
    
rule start
for P Y Z timeVal
rewrite
    {
    object P : process =
        {
            time : int = timeVal;       
            
        }
    object Y : activity = 
        {
            aS : activityState = (notStarted => inProgress);
            time : int = (0 => timeVal);
            linkToPredecessor : workSequence = {Z};         
        }   
    }   
when
    {
        Z.startedToStart->forAll(act| act.aS == inProgress);
        Z.finishedToStart->forAll(act| act.aS == finished);
        Y.resources->forAll(r| r.available == true);
    }   
then  
    {
        var r; 
        for (r <- Y.resources)
            {
                r.available   <- false ;
            }    
            
        print("start");
        print(Y);        
    }   

rule finish
for P Y Z timeVal1 timeVal2
rewrite
    {
    object P : process =
        {   
        
            time : int = timeVal1;
        }
    object Y : activity = 
        {
            aS : activityState = (inProgress => finished);
            linkToPredecessor : workSequence = {Z}; 
            time : int = timeVal2;  
        }    
    }   
when
    {
       Z.startedToFinish->forAll(act| act.aS == inProgress);
       Z.finishedToFinish->forAll(act| act.aS == finished);
    }   
then  
    {
        var x r;
        x <- (timeVal1 - timeVal2) ;
        if ( x < Y.tmin)
          {
            Y.tS <- tooEarly;
            print("tooEarly");
            print(Y);
          }
        else
          {
            if (x < (Y.tmax))
              {
                (Y.tS) <- ok;
                print("ok");
                print(Y);
              }
            else
              {
                (Y.tS) <- tooLate;
                print("tooLate");
                print(Y);
              }
          }  
        for (r <-Y.resources)
            {
                (r.available) <- true;
            } 
    }   

rule done
for P
rewrite
 {
object P:process = {}
 }
 when
 {
allInstances(activity)->forAll(a | a.aS == finished) ;
allInstances(activity)->forAll(a | a.tS == ok);
 }
 then
 {
  print("reached");
 }

